p, q:. p b q   

latex

ProofTree

Definitions	p b q, t  T, x:A. B(x)
Lemmas	bool wf, bnot wf, band wf, bor wf